The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
plus(s(x), y) →⁺ s(plus(x, y))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x / s(x)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)